(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-sort S0 0)
(declare-fun v0 () S0)
(declare-fun v1 () S0)
(declare-fun f0 ( S0) S0)
(declare-fun f1 ( S0 S0 S0) S0)
(declare-fun f2 ( S0 S0 S0) S0)
(declare-fun f3 ( S0 S0) S0)
(declare-fun f4 ( S0 S0) S0)
(declare-fun p0 ( S0 S0) Bool)
(declare-fun p1 ( S0 S0) Bool)
(declare-fun p2 ( S0 S0 S0) Bool)
(declare-fun p3 ( S0 S0) Bool)
(declare-fun p4 ( S0 S0) Bool)
(assert (let ((e2 (f4 v1 v1)))
(let ((e3 (f0 e2)))
(let ((e4 (f2 v0 v0 e3)))
(let ((e5 (f1 v0 e2 e4)))
(let ((e6 (f2 e3 e5 v0)))
(let ((e7 (f0 e5)))
(let ((e8 (f0 v0)))
(let ((e9 (f4 v0 v1)))
(let ((e10 (f0 e2)))
(let ((e11 (f3 e2 e3)))
(let ((e12 (p1 e11 e5)))
(let ((e13 (= v0 e11)))
(let ((e14 (p2 e7 e4 v1)))
(let ((e15 (= e9 v0)))
(let ((e16 (p4 e5 e2)))
(let ((e17 (p2 e10 e8 e11)))
(let ((e18 (p2 v1 e6 e2)))
(let ((e19 (p0 v0 e4)))
(let ((e20 (p3 e10 e11)))
(let ((e21 (p2 v0 e10 v0)))
(let ((e22 (distinct e3 e6)))
(let ((e23 (ite e15 v0 e9)))
(let ((e24 (ite e21 e8 e11)))
(let ((e25 (ite e18 e2 e7)))
(let ((e26 (ite e22 v1 e2)))
(let ((e27 (ite e18 e6 e24)))
(let ((e28 (ite e14 e27 e4)))
(let ((e29 (ite e17 e10 e4)))
(let ((e30 (ite e13 e3 e8)))
(let ((e31 (ite e19 e10 e25)))
(let ((e32 (ite e20 e5 e7)))
(let ((e33 (ite e13 e6 e7)))
(let ((e34 (ite e12 e7 e30)))
(let ((e35 (ite e12 e28 e24)))
(let ((e36 (ite e14 e3 e34)))
(let ((e37 (ite e15 e25 e30)))
(let ((e38 (ite e16 e10 e3)))
(let ((e39 (p0 e6 e36)))
(let ((e40 (p4 e30 e4)))
(let ((e41 (distinct e37 v0)))
(let ((e42 (p2 e11 e8 e10)))
(let ((e43 (= e29 e23)))
(let ((e44 (p2 e32 e31 e8)))
(let ((e45 (p1 e6 e33)))
(let ((e46 (= v1 e11)))
(let ((e47 (p3 e7 v0)))
(let ((e48 (p0 e4 e29)))
(let ((e49 (p0 e28 v1)))
(let ((e50 (p3 e38 e37)))
(let ((e51 (= e26 e28)))
(let ((e52 (p2 e3 e23 e9)))
(let ((e53 (distinct e35 e8)))
(let ((e54 (p3 e23 e36)))
(let ((e55 (= e34 e23)))
(let ((e56 (distinct e25 e33)))
(let ((e57 (p4 e32 e11)))
(let ((e58 (distinct e24 e26)))
(let ((e59 (distinct e2 e28)))
(let ((e60 (= e27 e27)))
(let ((e61 (p1 e6 e35)))
(let ((e62 (distinct e5 e36)))
(let ((e63 (not e58)))
(let ((e64 (and e19 e51)))
(let ((e65 (ite e55 e48 e64)))
(let ((e66 (ite e49 e15 e61)))
(let ((e67 (and e62 e45)))
(let ((e68 (ite e21 e22 e18)))
(let ((e69 (ite e50 e44 e56)))
(let ((e70 (or e59 e14)))
(let ((e71 (=> e69 e16)))
(let ((e72 (or e39 e70)))
(let ((e73 (=> e72 e52)))
(let ((e74 (or e66 e63)))
(let ((e75 (not e41)))
(let ((e76 (not e12)))
(let ((e77 (ite e73 e20 e54)))
(let ((e78 (not e74)))
(let ((e79 (or e47 e76)))
(let ((e80 (ite e71 e43 e79)))
(let ((e81 (= e53 e75)))
(let ((e82 (= e77 e57)))
(let ((e83 (xor e78 e68)))
(let ((e84 (=> e46 e13)))
(let ((e85 (or e40 e80)))
(let ((e86 (=> e81 e81)))
(let ((e87 (xor e42 e60)))
(let ((e88 (and e65 e65)))
(let ((e89 (=> e82 e85)))
(let ((e90 (= e17 e17)))
(let ((e91 (= e89 e83)))
(let ((e92 (and e90 e67)))
(let ((e93 (= e87 e88)))
(let ((e94 (not e91)))
(let ((e95 (or e94 e93)))
(let ((e96 (xor e86 e95)))
(let ((e97 (not e92)))
(let ((e98 (and e84 e97)))
(let ((e99 (and e96 e96)))
(let ((e100 (xor e99 e99)))
(let ((e101 (or e100 e98)))
e101
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
